Nuprl Definition : ecl-mng-update 11,40

ecl-mng-update{i:l}
ecl-mng-update(esidsdaxzupd)
== es-decls(es;i;ds;da)
==  alle-at(es;
==  alle-at(i;
==  alle-at(e.(es-after(esze)
==  alle-at(e.(=
==  alle-at(e.(list_accum(z',nf.let n,f = nf
==  alle-at(e.(list_accum(in
==  alle-at(e.(list_accum(if es-bact{i:l}
==  alle-at(e.(list_accum(if es-bact(dsdaxesn; es-init(es;e); e)
==  alle-at(e.(list_accum(then f(es-state-when(ese),es-val(ese))
==  alle-at(e.(list_accum(else z'
==  alle-at(e.(list_accum(fi ;
==  alle-at(e.(list_accum(es-when(esze);
==  alle-at(e.(list_accum(fpf-cap(upd;
==  alle-at(e.(list_accum(fpf-cap(product-deq(Knd; Id; Kind-deq; id-deq);
==  alle-at(e.(list_accum(fpf-cap(<es-kind(ese), z>;
==  alle-at(e.(list_accum(fpf-cap([])))) 
latex



clarification:

ecl-mng-update{i:l}
ecl-mng-update(esidsdaxzupd)
== es-decls(es;i;ds;da)
==  alle-at(es;
==  alle-at(i;
==  alle-at(e.(es-after(esze)
==  alle-at(e.(=
==  alle-at(e.(list_accum(z',nf.let n,f = nf
==  alle-at(e.(list_accum(in
==  alle-at(e.(list_accum(if es-bact{i:l}
==  alle-at(e.(list_accum(if es-bact(dsdaxesn; es-init(es;e); e)
==  alle-at(e.(list_accum(then f(es-state-when(ese),es-val(ese))
==  alle-at(e.(list_accum(else z'
==  alle-at(e.(list_accum(fi ;
==  alle-at(e.(list_accum(es-when(esze);
==  alle-at(e.(list_accum(fpf-cap(upd;
==  alle-at(e.(list_accum(fpf-cap(product-deq(Knd; Id; Kind-deq; id-deq);
==  alle-at(e.(list_accum(fpf-cap(<es-kind(ese), z>;
==  alle-at(e.(list_accum(fpf-cap([]))
==  alle-at(e.( fpf-cap(ds; id-deq; z; top))) 
latex


Definitions[], es-kind(ese), <ab>, id-deq, Kind-deq, Id, Knd, product-deq(ABab), fpf-cap(feqxz), es-when(esxe), es-val(ese), es-state-when(ese), f(a), es-init(es;e), es-bact{i:l}(dsdaaesne1e2), if b then t else f fi , let x,y = A in B(x;y), list_accum(x,a.f(x;a); yl), es-after(esxe), top, s = t, alle-at(esie.P(e)), es-decls(es;i;ds;da), P  Q
FDL editor aliasesecl-mng-update

origin